$\forall$$i$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $x$:Id, $k$:Knd, $T$:Type, ${\it test}$:(State(${\it ds}$)$\rightarrow$$T$$\rightarrow\mathbb{B}$).
\\[0ex]($\neg$($\uparrow$$x$ $\in$ dom(${\it ds}$)))
\\[0ex]$\Rightarrow$ (($\uparrow$isrcv($k$)) $\Rightarrow$ ($i$ = destination(lnk($k$))))
\\[0ex]$\Rightarrow$ Normal($T$)
\\[0ex]$\Rightarrow$ Normal(${\it ds}$)
\\[0ex]$\Rightarrow$ $\vdash$${\it es}$.recognizer(${\it es}$;$i$;${\it ds}$;$x$;$k$;$T$;${\it test}$)